| Definitions |  es.P(es), f(a), State(ds),  , weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f),   x. t(x), x.A(x),  , Id, "$x", P   Q,  x:A. B(x), Consistent(R;es), ES, R-Feasible(R), es realizer ind, s = t, Normal(ds), x dom(f). v=f(x) P(x;v),  b, x:A  B(x), a:A fp B(a), IdLnk, x:A  B(x), FinProbSpace, {x:A| B(x)} , Type, t T, weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), Outcome, @i Precondition for a:Outcome(p) is P:State(ds) , source(l), es-realizer(p), pre-p-realizable, A  B, locl(a),  x:A.B(x),   b, Realizer, rec(x.A(x)),  , Knd, Rpre(loc;ds;a;p;P), Rsframe(lnk;tag;L), Rsends(ds;knd;T;l;dt;g), Void, #$n, l[i], i  z j, i <z j, hd(l), <a, b>, f(x)?z, False, x : v, [], [car / cdr], DeclaredType(ds;x), IdDeq, if b then t else f fi , left + right, Unit, P  Q, A, {i..j },  , A B, i j < k, P & Q, a < b, ||as||,  , type List, Top, Atom$n, usends1-p(es;ds;k;T;l;tg;B;f), isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), isrcv(k), x dom(f), f(x), kind(e), x,y. t(x;y), first(e), suptype(S; T),  x:A. B(x), usends1-p-realizable, destination(l), lnk(k), tag(k), S T, EqDecider(T), EOrderAxioms(E; pred?; info), Msg(M), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, e < e', kindcase(k; a.f(a); l,t.g(l;t) ), constant_function(f;A;B), loc(e), SWellFounded(R(x;y)), pred!(e;e'), EState(T), tl(l), Normal(T), e@i. P(e), only events in L send on l with tg, sframe-p-realizable, A c B, vartype(i;x), E, valtype(e), P  Q, e loc e' , e c e', rcv(l,tg), kind(e), let x,y = A in B(x;y), sender(e), t.1, (x l), e' e.P(e'), isrcv(e), {T}, P Q, s ~ t, SQType(T), loc(e), val(e),  , (state when e), state@i, @i discrete ds,  T, True, case b of inl(x) => s(x) | inr(y) => t(y), lnk(e), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), first(e), t ...$L, Dec(P), qeq(r;s), tt, EquivRel(T;x,y.E(x;y)), A  B,  , (state after e)+t, x,y:A//B(x;y), (e < e'), (e <loc e'), Trans(T;x,y.E(x;y)) |
| Lemmas | es-le weakening eq, es-le transitivity, es-causle-trans, es-causle wf, es-state-after-elapsed wf, true wf, btrue wf, qeq wf2, int nzero wf, b-union wf, quotient wf, es-le wf, es-locl wf, es-causl wf, es-le-loc, Id sq, decidable es-le, decidable equal Kind, decidable cand, es-causle weakening locl, es-loc-rcv, es-first wf, es-loc-pred, IdLnk sq, squash wf, es-causle weakening, es-causl transitivity1, es-sender-causl, es-vartype wf, es-state-subtype, es-loc wf, es-state-subtype2, es-state-when wf, bool sq, bool cases, es-val wf, member wf, Knd sq, es-isrcv-loc, es-kind-rcv, es-sender wf, es-kind wf, member singleton, rcv wf, es-E wf, sframe-p wf, sframe-p-realizable, constant function wf, val-axiom wf, usends1-p wf, tagof wf, lnk wf, ldst wf, first wf, EState wf, kindcase wf, qle wf, cless wf, Msg wf, loc wf, kind wf, EOrderAxioms wf, deq wf, fpf-trivial-subtype-top, fpf-ap wf, fpf-dom wf, usends1-p-realizable, natural number wf p-outcome, normal-type wf, isrcv wf, false wf, length wf nat, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, eqof eq btrue, fpf-cap-single, fpf-cap-single1, ifthenelse wf, le wf, fpf-single wf, Rsends wf, Rpre wf, decl-type wf, Knd wf, rationals wf, unit wf, select member, top wf, id-deq wf, fpf-cap wf, nat wf, not wf, bnot wf, es realizer wf, Rsframe wf, locl wf, R-sub-Rlist, es-realizer wf, es-real wf, pre-p wf, lsrc wf, pre-p-realizable, R-sub-implies, es-real-implies, R-consistent wf, event system wf, p-outcome wf, weak-precond-send-p wf, implies-es-real, weakPrecondSendR2 feasible, weakPrecondSendR2 wf, finite-prob-space wf, IdLnk wf, Id wf, fpf wf, bool wf, decl-state wf, assert wf, normal-ds wf |
f:({s:State(ds)|